The present invention relates generally to circuit design verification, and more particularly to structural circuit design verification.
In the design of digital integrated circuits, it is often desirable to be able to ascertain whether two circuits are equivalent. In particular, the determination of circuit equivalency has become increasingly important with the emergence of large scale digital integrated circuits that incorporate an entire system on a chip. Such chips have reached a size and complexity level where it is difficult to verify them, in a timely manner, using traditional gate-level simulation. As a result, static verification tools are being more widely utilized by chip designers. Examples of such static-verification tools are PrimeTime, a static-timing analyzer, and Formality, a formal verification tool. Both PrimeTime and Formality are products of Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Static-timing analysis is used to analyze and verify the timing of the design and formal verification is used to verify a design""s functionality by proving functional equivalence.
A design methodology that utilizes formal verification can reduce the number of time-consuming gate-level simulation runs. In a typical design process, utilizing logic synthesis and formal verification tools, the designer specifies his or her initial design at the register-transfer level (RTL). This RTL source specification is translated into a gate-level netlist by a logic synthesis tool, such as Design Compiler, produced by Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Formal verification is then used to compare the functional equivalency of the RTL source specification to the post-synthesis gate-level netlist. This gate-level netlist may then undergo several succeeding transformations that are intended to produce equivalent gate-level netlists. Such succeeding transformations can include: scan chain insertion, clock-tree synthesis, in-place optimization and manual editing. After each of these succeeding transformations, formal verification can be used to verify that the result of the latest transformation is functionally equivalent to the resulting gate-level netlist of the preceding transformation. For each of these comparisons a known-to-be-correct design (reference design) is compared against a design of unknown correctness (implementation design).
Formality operates by identifying xe2x80x9ccompare pointsxe2x80x9d which are points in the reference and implementation designs that are examined for equivalency. If all compare points in the implementation design are found equivalent to a corresponding compare point in the reference design, then the two designs are, in total, equivalent to each other.
Three major components comprise the Formality architecture: a verification manager, a suite of verification solvers and a debug analyzer. The verification manager is responsible for determining the corresponding compare point of the reference design that should be compared for functional equivalency against each compare point of the implementation design. The verification manager also determines the logic cone for each compare point. The logic cone for each compare point is found by following each compare point""s transitive fanin until a primary input, or another compare point, is reached. These primary inputs or compare points, which define the transitive fanin boundary of a compare point, shall be referred to as the compare point""s logic cone inputs. In addition to determining the corresponding compare point of the reference design, for each compare point of the implementation design, the verification manager also xe2x80x9calignsxe2x80x9d the logic cone inputs for such paired compare points. The verification manager accomplishes this by determining the logic cone input of the reference design""s compare point, that should be correspond to each logic cone input of the implementation design""s compare point, when functional equivalency of the compare points for the two logic cones is being determined.
Once such compare point matching and logic cone input alignment has been determined, algorithms to determine equivalency can be applied. Formality chooses the most appropriate equivalency-determining algorithm (referred to as a xe2x80x9csolverxe2x80x9d) from its suite of verification solvers. For example, a binary decision diagram (BDD) based solver may be used for compare points driven by complex control logic, but other algorithms may be more efficient for data path circuits.
Equivalency of two combinational circuits can be defined, in a functional sense, as follows. The reference and implementation designs are equivalent if both accept the same set of input combinations, and if both produce the same output combination for each input combination. Equivalency can also be defined, in a less strict sense, if don""t cares are allowed in the reference design""s input combinations. In that case, the implementation design only needs to define the same function over those input patterns for which the reference design is defined.
If Formality discovers errors during the verification process, the designer can identify nets or instances of the implementation design that may be responsible for the errors with the Formality debug analyzer.
Determining the corresponding compare points between the reference and implementation designs, and aligning the logic cone inputs of the compare points, is important for formal verification systems, such as Formality, since it permits the relatively computationally expensive equivalency-determining algorithms to be strategically applied. It would therefore be desirable to improve the speed and specificity with which such compare point correspondences, and logic cone alignments, can be found.
For purposes of describing the present invention, the determination of compare point correspondences, and logic cone input alignments, shall be referred to as the determination of xe2x80x9cnecessary correspondencesxe2x80x9d between inputs or outputs of the two circuits to be compared. A necessary correspondence between a first output of a first circuit and a first output of a second circuit indicates that both the following statements are true: i) if the first output of the first circuit is equivalent to an output of the second circuit, then that equivalent output must be the first output of the second circuit; and ii) if the first output of the second circuit is equivalent to an output of the first circuit, then that equivalent output must be the first output of the first circuit. A necessary correspondence between a first input of a first circuit and a first input of a second circuit indicates that both the following statements are true: i) if the first input of the first circuit is equivalent to an input of the second circuit, then that equivalent input must be the first input of the second circuit; and ii) if the first input of the second circuit is equivalent to an input of the first circuit, then that equivalent input must be the first input of the first circuit. These necessary correspondences are so called because while they establish necessary conditions for equivalency to occur, they are not sufficient to determine that equivalency actually exists.
Once such necessary correspondences have been determined, algorithms to determine actual equivalency can be more strategically applied. The present invention comprises a method for determining such necessary correspondences in an efficient way such that the cost of utilizing it is often much smaller than the cost of utilizing equivalency-determining methods. Therefore, it is often cost-effective (i.e. more efficient), as part of an equivalency-determining circuit design tool, to first apply the teachings of the present invention in order to lessen subsequent application of an equivalency determining method.
The present invention presents an efficient method for finding necessary correspondences between the combinational portions of two circuit designs utilizing a graph-coloring algorithmic approach applied to a simplified bipartite representation of the two circuits to be matched.
The major steps of the necessary correspondences procedure of the present invention are as follows.
The bipartite representation is determined for each circuit to be compared. Each bipartite representation is comprised of a left set of nodes, a right set of nodes and a set of edges which connect the nodes of the left and right sets. Primary inputs and primary outputs of a circuit are represented, respectively, by nodes in the left set and nodes in the right set of the simplified representation. Other xe2x80x9cinputxe2x80x9d and xe2x80x9coutputxe2x80x9d nodes also need to be represented in the left and right sets in order that a matching of the combinational circuitry be performed by the invention. In particular, registers internal to the circuits to be matched result in left and right nodes of their simplified representations. Inputs to a register become outputs in the bipartite representation, since they are connected to outputs of combinational circuitry, and are put in the right set of the circuit""s bipartite representation. Outputs from a register become inputs in the bipartite representation, since they are connected to inputs of combinational circuitry, and are put in the left set of the circuit""s bipartite representation.
The approach to matching of the present invention is xe2x80x9cstructuralxe2x80x9d matching in the sense that it is these bipartite graph structures which are being matched with each other. Any input circuit design representation, from which such a bipartite graph representation can be determined, can be matched for necessary correspondences with the present invention.
The bipartite representation is xe2x80x9cprimedxe2x80x9d by coloring the nodes of each circuits"" left and right sets on the basis of information known about the circuits. Three main strategies for priming are utilized, with the unifying principle, of all three strategies, that any two nodes which could potentially be identified as having a necessary correspondence with each other cannot be primed with different colors.
Consistency and progress checks of the primed bipartite representation are made as follows.
In general, consistency checks determine whether the coloring that has just been accomplished has resulted in matching nodes (i.e. nodes which in fact share a necessary correspondence) or in invalid nodes (i.e. nodes which are treated as not having a necessary correspondence). A xe2x80x9cmatchxe2x80x9d is defined to have occurred if two nodes, one from each circuit, are: i) both in the same left or right side of their respective circuit, and ii) both possess the same unique color with respect to all other nodes on their side of the circuits.
The following first application of the consistency checking procedure, following the initial priming of the nodes, is first applied with respect to one side of both circuits and is then applied to the other side of both circuits. As will be discussed below, all further applications of the consistency checking procedure, having occurred after at least one application of the recoloring procedure, are applied only to the side of both circuits which has just been recolored.
All xe2x80x9cmaximal uniform groupsxe2x80x9d of one or more nodes are identified on the same side of each circuit. A maximal uniform group is one in which all of its nodes share the same color, and no other nodes, of that side of that circuit, have the same color. For all maximal uniform groups containing only one node, if there is a maximal uniform group for the same side of the other circuit having the same color and same number of nodes (one node), then both groups are indicated as having matched nodes. For each maximal uniform group of one or more nodes, if there exists no maximal uniform group for the same side of the other circuit having the same color, then all nodes of the maximal uniform group are colored invalid. For each maximal uniform groups of two or more nodes, if there exists a maximal uniform group for the same side of the other circuit having the same color, but having a different number of nodes, then all nodes in both maximal uniform groups are colored invalid.
Progress checks determine whether the procedure for identifying necessary correspondences should continue. While more complex progress checks are performed later in this process, at this point in the procedure the progress check merely determines whether all nodes have already been matched. If they have been (an unlikely event), then no further identification of necessary correspondences is performed. If all nodes have not already been matched, then the recoloring procedure is executed.
The recoloring procedure operates as follows. Each time the recoloring procedure is executed, it alternates between the side of each circuit which is recolored. When called initially, the side to be recolored is arbitrarily chosen. The side to be recolored shall be referred to as the xe2x80x9ctargetxe2x80x9d side, and the side serving purely as data for recoloring the target shall be referred to as the xe2x80x9csourcexe2x80x9d side. Recoloring is performed on a node-by-node basis for each node of the target side. The current node of the target side to be recolored shall be referred to as the xe2x80x9ctarget node.xe2x80x9d The nodes on the source side, which are connected by an edge to the target node, shall be referred to as xe2x80x9csource nodes.xe2x80x9d The general default rule for recoloring each target node is that it gets its own previous color value, plus the sum of the values of each of its source nodes.
Consistency and progress checks are then performed of the just recolored sides. As discussed above, the consistency checking procedure looks for nodes which should be marked as matched or nodes which should be marked invalid. It should be noted, however, that the consistency checking procedure described above is applied, at this point in the overall necessary correspondences procedure, only to the side of both circuits which has just been recolored. The progress check then performs tests to determine whether the necessary correspondences procedure should be terminated, or whether it should continue for at least another iteration by looping back to perform another recoloring step.
Progress checks are then performed as follows. The results of the progress checks are to set certain progress indicators. If all nodes on both sides of both circuits are marked as having been matched, following the just-previous consistency check, then an xe2x80x9call-matchedxe2x80x9d progress indicator is set. In addition to this xe2x80x9call-matchedxe2x80x9d progress indicator, the following progress checks also determine whether a xe2x80x9cside-progressxe2x80x9d progress indicator should be set. If at least one new match has been identified, by the just-previous consistency check, then the xe2x80x9cside-progressxe2x80x9d progress indicator, for the side of the circuits just recolored, is set. If at least one new invalid node has been identified, by the just-previous consistency check, then the xe2x80x9cside-progressxe2x80x9d progress indicator, for the side of the circuits just recolored, is set. A count is also performed of the number of maximal uniform groups, for the circuit sides that have just been recolored and consistency checked. If this count is greater than the last time this count was taken, after the same side of the same circuit was last recolored and consistency checked, then the xe2x80x9cside-progressxe2x80x9d progress indicator, for the side of the circuits just recolored, is set.
A check is then made to determine whether the xe2x80x9call-matchedxe2x80x9d progress indicator has been set. If the result of this query is positive, then the procedure for necessary correspondences determination is terminated. If the result of this query is negative, then a check is made to determine whether the xe2x80x9cside-progressxe2x80x9d progress indicator, for the just-recolored circuit side, has been set. If the result of this query is positive, then the necessary correspondences procedure continues by looping back for another execution of the recoloring procedure. If the result of this query is negative, then a check is made to determine whether the xe2x80x9cside-progressxe2x80x9d progress indicator, for the side opposite to the side just-recolored, has been set. If the result of this query is positive, then the necessary correspondences procedure continues by looping back for another execution of the recoloring procedure. If the result of this query is negative, then the determination of necessary correspondences is halted due to the lack of progress.
Advantages of the invention will be set forth, in part, in the description that follows and, in part, will be understood by those skilled in the art from the description or may be learned by practice of the invention. The advantages of the invention will be realized and attained by means of the elements and combinations particularly pointed out in the appended claims and equivalents.